ds:x:Id fp Type, da:k:Knd fp Type, x:ecl(ds;da), m:. ecl-act(ds;da;m;x)(nil)  False 

latex

Definitions

x:A. B(x), , P  Q, ecl-act(ds;da;m;x), False, Prop, P  Q, t  T, x. t(x), P  Q, x:A. B(x), P & Q, P  Q, AB, A, SQType(T), {T}, x(s), star-append(T;P;Q), if b t else f fi, true, false, S  T

Lemmas

ecl-induction, nat wf, iff wf, ecl-act wf, event-info wf, false wf, ecl wf, decl-state wf, ma-valtype wf, bool wf, append is nil, append wf, ecl-halt wf, le wf, nat plus wf, iseg wf, nat plus inc, star-append wf, ifthenelse wf, eq int wf, fpf wf, Knd wf, Id wf, concat wf, bool cases, bool sq, iff transitivity, assert wf, eqtt to assert, assert of eq int, ecl-halt-nil, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff